spec: `ECSM` by erik-3milabs · Pull Request #655 · yetanotherco/lambda_vm

erik-3milabs · 2026-06-09T09:43:54Z

This PR introduces the ECSM (Elliptic Curve Scalar Multiplication) accelerator.

github-actions · 2026-06-09T09:46:58Z

Codex Code Review

Findings

High: inactive EC_SCALAR rows emit SERVE_K tokens. In spec/src/ec_scalar.toml, the recursive SERVE_K interaction uses multiplicity = ["not", "last_limb"], independent of μ. Since line 99 forces last_limb = 0 when μ = 0, every inactive/padding row emits a free SERVE_K token. Those can be consumed by active scalar rows and produce BIT tokens not rooted in the ECSM request’s addr_k, breaking the binding between k and the double-and-add sequence. Gate this by activity, e.g. μ * (1 - last_limb) or μ - last_limb with the existing implication.
High: ECDAS lambda carry recurrence uses c0[0] instead of c0[i]. In spec/src/ecdas.toml, the i = 1..63 lambda constraint starts with 2^8 * c0[0]. The rendered constraint and carry pattern require 2^8 * c0[i]. As written, most lambda carry limbs are not tied into the recurrence correctly, so the modular relation for λ is underconstrained for higher limbs. This can let invalid EC add/double steps satisfy the spec.

No other concrete PR-diff issues found in this pass.

claude · 2026-06-09T09:49:27Z

+ref = "ec:a:addr_k_alignment"
+
+[[assumptions]]
+desc = "$(#`addr_xR` mod 2^32) + 24 < 2^32$"


Low — Inconsistent assumption bound for addr_k

k is 32 bytes, read in four 8-byte chunks at offsets 0, 8, 16, 24 — the same access pattern as xG. The assumption for addr_xG correctly uses + 24, but this one says + 31. The bound should be + 24 for consistency and to match what is actually constrained.

Suggested change

desc = "$(#`addr_xR` mod 2^32) + 24 < 2^32$"

desc = "$(#`addr_k` mod 2^32) + 24 < 2^32$"

This + 31 is on purpose, to make sure the EC_SCALAR chip doesn't trip up.
This comment can be disregarded.

claude · 2026-06-09T09:49:51Z

Code Review — ECSM Accelerator Spec

Good overall structure. The three-chip decomposition (ECSM → ECDAS → EC_SCALAR) is clean, and the soundness argument for why the point-at-infinity can never appear during double-and-add is well-reasoned.

Issues found

Mathematical error (spec/ecsm.typ:23)
The non-singularity condition is written as $a^3+27b^2 \neq 0$, but the correct Weierstrass discriminant is $4a^3+27b^2 \neq 0$. Harmless for secp256k1 (a=0) but incorrect in general. See inline comment.

Typo (spec/ecsm.typ:158)
$q_0 \in [0, 2p)$ should be $q_1 \in [0, 2p)$ — copy-paste error in the quotient bound discussion.

Ref typo (spec/src/ecdas.toml:316)
"ecda:c:range_c0" is missing the trailing s — should be "ecdas:c:range_c0".

Assumption inconsistency (spec/src/ecsm.toml:199)
The alignment assumption for addr_k uses + 31 but the actual memory reads are in four 8-byte chunks at offsets 0, 8, 16, 24 — identical to addr_xG and addr_xR, which both use + 24. The bound should be + 24 for consistency.

Minor observations

The doubling formula is silently specialized to a=0; the general theory section (which still writes E(a,b,p)) could note this specialization explicitly.
Several new files are missing a trailing newline (about_ecalls.typ, ec_scalar.toml, ecdas.toml).
The aside explaining why y_A != 0 for secp256k1 says "as previously established" but the establishment is not in this document — citing the odd-order argument explicitly would make it self-contained.

erik-3milabs · 2026-06-09T10:21:25Z

Codex Code Review

Findings

High: inactive EC_SCALAR rows emit SERVE_K tokens. In spec/src/ec_scalar.toml, the recursive SERVE_K interaction uses multiplicity = ["not", "last_limb"], independent of μ. Since line 99 forces last_limb = 0 when μ = 0, every inactive/padding row emits a free SERVE_K token. Those can be consumed by active scalar rows and produce BIT tokens not rooted in the ECSM request’s addr_k, breaking the binding between k and the double-and-add sequence. Gate this by activity, e.g. μ * (1 - last_limb) or μ - last_limb with the existing implication.

Indeed. Fixed it.

High: ECDAS lambda carry recurrence uses c0[0] instead of c0[i]. In spec/src/ecdas.toml, the i = 1..63 lambda constraint starts with 2^8 * c0[0]. The rendered constraint and carry pattern require 2^8 * c0[i]. As written, most lambda carry limbs are not tied into the recurrence correctly, so the modular relation for λ is underconstrained for higher limbs. This can let invalid EC add/double steps satisfy the spec.

Fixed it

erik-3milabs · 2026-06-09T10:24:31Z

Code Review — ECSM Accelerator Spec

Minor observations

The doubling formula is silently specialized to a=0; the general theory section (which still writes E(a,b,p)) could note this specialization explicitly.

Technically, this is already addressed: the introduction mentions that it accelerates points in E(0, b, p)

Several new files are missing a trailing newline (about_ecalls.typ, ec_scalar.toml, ecdas.toml).

Fixed

The aside explaining why y_A != 0 for secp256k1 says "as previously established" but the establishment is not in this document — citing the odd-order argument explicitly would make it self-contained.

It is in the same document, but a section earlier. Disregarding the comment.

RobinJadoul

I do wonder how much potential optimization we're leaving on the table by treating p as a generic prime, rather than using the structure it has
A more descriptive name for the BIT and SERVE_K interactions may be in order
The complex arith constraints for equalities mod p tend to have a different order between their "constraint" and "poly", which makes checking correspondence a bit tedious and error-prone
I have some thoughts about the presentation of the "theory"/background, but trying to focus on the more technical things first

RobinJadoul · 2026-06-09T12:46:23Z

+/ -2: `KECCAK` (@keccak)
+/ -3: `ECSM` (@ecsm)


Maybe interesting to make this -11 instead, so that we essentially reserve some extra space for more hashes?

RobinJadoul · 2026-06-10T11:49:27Z

+desc = "$(#`addr_xG` mod 2^32) + 24 < 2^32$"
+ref = "ec:a:addr_xG_alignment"
+
+[[assumptions]]
+desc = "$(#`addr_k` mod 2^32) + 31 < 2^32$"
+ref = "ec:a:addr_k_alignment"
+
+[[assumptions]]
+desc = "$(#`addr_xR` mod 2^32) + 24 < 2^32$"
+ref = "ec:a:addr_xR_alignment"


How safe is this? The fact that this comes from an ECALL means that it is not an assumption we can ensure at the spec level, and rather something that is pushed down into the guest program.

RobinJadoul · 2026-06-10T12:21:44Z

+Note: `xG` is assumed to be range checked, since they're read from memory.
+#render_constraint_table(ecsm_chip, config, groups: "read_xG")
+
+=== Constrain `Gy`


Suggested change

=== Constrain `Gy`

=== Constrain `yG`

For consistency

RobinJadoul · 2026-06-10T12:29:43Z

+This accelerator instead leverages the _double-and-add_ #footnote(link("https://en.wikipedia.org/wiki/Elliptic_curve_point_multiplication#Double-and-add")) technique, which utilizes only $O(log(k))$ additions for the full multiplication.
+
+#strong("This accelerator.")
+The purpose of this accelerator is to speed up the scalar multiplication $k times G$ for scalar $k in [1, N)$ and point $G in E(0, b, p) without {#inf}$ with $p in [2^248, 2^256)$.


Does it stop working for p < 2^248, or is it just wasteful?

RobinJadoul · 2026-06-10T14:07:07Z

+[[variables.input]]
+name = "ptr"
+type = "DWordWL"
+desc = "pointer to the first byte of the scalar"
+pad = 0


Why are we doing a bunch of MEMWs in this chip? The calling ECSM has already read all of K into byte limbs, so we can just take in the limb as input and decompose it, right?

I guess the reason is that EC_SCALAR recurses onto itself, reducing the interactions in the ECSM table, but I think for total area it'd be better feed in the bytes directly; at which point, there may be some tradeoff between how many bits EC_SCALAR does at once for width vs depth, but again probably total area tells us to just make it 256 wide?
In the case 256 columns wide wouldn't be the right call, just making multiple calls into EC_SCALAR from ECSM should nevertheless still be the same area cost as the recursion, but simpler because there's no recursion logic to be performed.

There may even be some approach where we avoid the recursion of ECDAS as well, and simply let the EC_SCALAR chip emit the sequence of double/add steps that need to be performed. Not entirely sure if that wouldn't introduce too many more interactions atm, but it's potentially cleaner than having to reason about the recursion stopping.

RobinJadoul · 2026-06-11T13:42:24Z

+
+We now explore this carry-technique and provide some proofs.
+
+== Lemma 1


Feels a bit weird to have manual lemma/corollary numbering in the a title. Probably best to switch to some typst package for those, if we're intending to formalize/prove more anyway.

RobinJadoul · 2026-06-11T13:47:50Z

+[[constraints.yR]]
+kind = "interaction"
+tag = "IS_HALF"
+input = [["+", ["idx", "c2", "i"], 16320]]


Can we maybe move these magic constant columns into a constant column of the chip? It's nicer to have them all in the same place to check correspondence with the analysis and make sure everything is up-to-date if we do change the analysis at some point (e.g. because we get Half limbs)

RobinJadoul · 2026-06-11T13:49:30Z

+Introducing non-negative witnesses $q''_0$ and $q''_1$, we convert these into
+$
+  2lambda y_A - 3x_A^2 + (#`r` - q''_0) p &= 0,\
+  lambda^2 - 2x_A - x_G - x_R + (#`r` - q''_1) p &= 0.\


Having x_G in there looks wrong and propagates a bit further

RobinJadoul · 2026-06-11T14:46:40Z

+kind = "interaction"
+tag = "BIT"
+input = ["timestamp", "round"]
+multiplicity = ["-", "next_op"]


I'd keep the positive here and the negative in EC_SCALAR, to keep with the usual interpretation of μ = -1 meaning that you've "shown" the relation to hold

RobinJadoul · 2026-06-11T14:53:41Z

+[[constraints.send]]
+kind = "template"
+tag = "IS_BIT"
+input = ["next_op"]
+ref = "ecdas:c:range_next_op"


The LogUp should take care of it, but probably good to still bit-check op itself too

Co-authored-by: claude[bot] <209825114+claude[bot]@users.noreply.github.com>

erik-3milabs requested a review from RobinJadoul June 9, 2026 09:43

erik-3milabs self-assigned this Jun 9, 2026

erik-3milabs added the spec Updates and improvements to the spec document label Jun 9, 2026

claude Bot reviewed Jun 9, 2026

View reviewed changes

Comment thread spec/ecsm.typ Outdated

claude Bot reviewed Jun 9, 2026

View reviewed changes

Comment thread spec/ecsm.typ

claude Bot reviewed Jun 9, 2026

View reviewed changes

Comment thread spec/src/ecdas.toml Outdated

claude Bot reviewed Jun 9, 2026

View reviewed changes

erik-3milabs commented Jun 9, 2026

View reviewed changes

Comment thread spec/ecsm.typ Outdated

Comment thread spec/ecsm.typ

erik-3milabs force-pushed the spec/ecsm branch from b96cdfd to a295377 Compare June 11, 2026 13:23

RobinJadoul reviewed Jun 11, 2026

View reviewed changes

RobinJadoul force-pushed the spec/main branch from 5a09d70 to a6ef9d1 Compare June 11, 2026 15:23

erik-3milabs added 15 commits June 12, 2026 08:50

spec/EC: introduce ECSM

884c5ad

spec/ECSM: introduce EC_SCALAR

1c274bd

spec/ECSM: introduce ECDAS

d2d08d8

spec/ECSM: two carry proofs

3a46d5a

spec/ECSM: update lemma

bd64b62

spec/ECSM: carry computation tool

d098975

spec/ECSM: fix lint issues

47a5be3

spec/ECSM: update extension names

b9530a9

spec/ECSM: update introduction

5ae2283

Spec/ECSM: update ecsm to work with offsets

e3848b5

spec/ECDAS: update non-inf argumentation

fe4e3dd

spec: fix cwrap for repeated subtractions

7e12156

spec/ECSM: tweaks and fixes

7988057

spec/ECSM: fix scalar read/serve timestamp

6db8da4

spec/ecsm: more tweaks and fixes

aab3904

erik-3milabs and others added 11 commits June 12, 2026 08:50

spec/ECSM: update carries

0a9d87e

spec/ECSM: drop carry.py

d9a1c3e

Apply suggestions from code review

33d65ea

Co-authored-by: claude[bot] <209825114+claude[bot]@users.noreply.github.com>

Update spec/ecsm.typ

bac746b

spec/ECSM: fix incorrect carry index

f604cd5

spec/ECSM: fix recursive SERVE_K multiplicity

18a815a

spec/ECSM: define padding

d7cefb2

spec/ECSM: fix missing trailing emptyline

1b4a50d

spec/ECDAS: fix missing multiplicity range check

1764697

spec/ECDAS: fix BIT-interaction multiplicity negation

93c7eb0

spec/ECSM: fix padding bug

33e846e

erik-3milabs force-pushed the spec/ecsm branch from a295377 to 33e846e Compare June 12, 2026 06:51

	desc = "$(#`addr_xR` mod 2^32) + 24 < 2^32$"
	desc = "$(#`addr_k` mod 2^32) + 24 < 2^32$"


		We now explore this carry-technique and provide some proofs.

		== Lemma 1

Conversation

erik-3milabs commented Jun 9, 2026

Uh oh!

github-actions Bot commented Jun 9, 2026

Codex Code Review

Uh oh!

Uh oh!

Uh oh!

Uh oh!

claude Bot Jun 9, 2026

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

claude Bot commented Jun 9, 2026

Code Review — ECSM Accelerator Spec

Issues found

Minor observations

Uh oh!

Uh oh!

Uh oh!

erik-3milabs commented Jun 9, 2026

Codex Code Review

Uh oh!

erik-3milabs commented Jun 9, 2026

Code Review — ECSM Accelerator Spec

Minor observations

Uh oh!

RobinJadoul left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants